#include "backtracking.h"
#include <vector>
#include <fstream>

// var is the current variable for which we have successfully
// found a value. This function looks for the next variable
// to instantiate.

using namespace std;


//is the global value index given by val currently free?
bool BT::validValue(int val)
{
	if(isAssigned(val/d))
		return false;
	Domain *dp=vars[val/d].dp;
	if(dp[val%d+1].yes)
		return true;
	return false;
}

int BT::lex()
{
	return phase;
}

//DOM: minimum domain variable selector
int BT::dom(){
  
  int varWithMinDomain = -1, minDomainSize = d+1;

  // choose the min domain
  for(int i=0; i<n; i++){
    if (!isAssigned(i) && (vars[i].domainSize < minDomainSize)){
      minDomainSize = vars[i].domainSize;
      varWithMinDomain = i;
    }
  }
  
  return varWithMinDomain; 
}

//DEG: maximum degree variable selector
int BT::deg(){
	
	int varWithMaxDegree = -1, maxDegSize=-1;
	
	for(int i=0; i<n; i++){
		int currVarDeg=cross_link_list[i].size();
		if (!isAssigned(i) && currVarDeg>maxDegSize){
				maxDegSize = currVarDeg;
				varWithMaxDegree = i;
		}
	}
	
	return varWithMaxDegree;
}

//FUTDEG: maximum future degree variable selector
//future degree is the current degree of a variable,
//equal to the number of unassigned neighbors
int BT::futdeg(){
	
	int varWithMaxDegree = -1, maxDegSize=-1;
	
	for(int i=0; i<n; i++){
		if (!isAssigned(i) && (vars[i].degree>maxDegSize)){
			maxDegSize = vars[i].degree;
			varWithMaxDegree = i;
		}
	}
	
	return varWithMaxDegree;
}

//Dom/Deg: Domain divided by degree.  smaller is better.
int BT::DD(){
	
	int bestVar = -1;
	double bestHeuristic=(d/.000001)+2;//the maximum possible heuristic value is a 
								//variable with no contraints and a full domain
							
	for(int i=0; i<n; i++){
		double currHeur=(double)vars[i].domainSize / (cross_link_list[i].size() + .000001);
		if (!isAssigned(i) && currHeur<bestHeuristic){
			bestHeuristic = currHeur;
			bestVar = i;
		}
	}
	return bestVar;
}


//Dynamic Dom/Deg: Domain divided by future degree.  smaller is better.
int BT::DyDD(){
	
	int bestVar = -1;
	double bestHeuristic=(d/.000001)+2;//the maximum possible heuristic value is a 
							//variable with no contraints and a full domain
							
	for(int i=0; i<n; i++){
		double currHeur=(double)vars[i].domainSize / (vars[i].degree + .000001);
		if (!isAssigned(i) && (currHeur<bestHeuristic)){
			bestHeuristic = currHeur;
			bestVar = i;
		}
	}
	return bestVar;
}

//Neighborhood-based variable selection.  This is an incarnation of the generalized
//neighborhood algorithm.  Uses Dom/Deg as the tightness function, + as the 
//combination operator, and goes only one level deep.
int BT::H_1_DD_plus(){
	
	int bestVar = -1;
	double bestHeuristic = -1;
	
	static vector<float> rating(n);
	
	for(int i=0; i<n; i++){
		if (!isAssigned(i)){
			rating[i] = vars[i].domainSize / (vars[i].degree+.0000001);
		}
	}

	for(int i=0;i<n;i++){
		if(!isAssigned(i)){
			double currentHeuristic = 0;
			if(vars[i].domainSize==1){
				currentHeuristic=2*d;
			}
			else if(vars[i].degree<2){
				currentHeuristic=2*d;
			}
			else{
				for(list<int>::iterator iter=cross_link_list[i].begin(); iter!=cross_link_list[i].end(); iter++){
					if(!isAssigned(*iter)){
						currentHeuristic += rating[*iter];
					}
				}
				currentHeuristic+=vars[i].domainSize;
			}
			currentHeuristic /= (vars[i].degree * vars[i].degree +.0000001);
			if(currentHeuristic < bestHeuristic || bestHeuristic==-1){
				bestHeuristic = currentHeuristic;
				bestVar = i;
			}
		}
	}
	//cout << endl;
	return bestVar;
}

//Pagerank: uses "pagerank" variable sorting.  In essence, this is very similar
//to a non-specific depth neighborhood search.  The actual pagerank mathematics
//do not tend well to a non-directed graph.
int BT::pagerank3(){

	static vector<int> nextVar(n);
	
	if(!hasRanked)
	{
		//ofstream delta("delta");
		vector<double> currRate(n);
		vector<double> nextRate(n);
		vector<bool> used(n);
		vector<int> degree(n);
		int totalEdges=0;
		for(int i=0;i<n;i++){
			used[i]=false;
			degree[i]=vars[i].degree;
			totalEdges+=degree[i];
		}
		
		for(int VPC=0;VPC<n;VPC++){  //Variable Phase Counter
			
			for(int i=0;i<n;i++){
				if(!used[i]){
					nextRate[i]=0;
					currRate[i]=degree[i];
					
				}
			}
			if(totalEdges>0){
				for(int i=0;i<n;i++){
					currRate[i]/=totalEdges;
				}
			}
			double total;
			bool running=true;
			int runs=0;
			while(running && runs<n*n){
				running=false;
				total=0;
				for(int i=0; i<n; i++){
					if(!used[i]){
						for(list<int>::iterator iter=cross_link_list[i].begin(); iter!=cross_link_list[i].end(); iter++){
							if(!used[*iter]){
								nextRate[i]+=currRate[*iter]+currRate[i];
							}
						}
						total+=nextRate[i];
					}
				}
				for(int i=0;i<n;i++){
					if(!used[i]){
						if(total>0){
							nextRate[i]/=total;
						}
						double tD=currRate[i]-nextRate[i];
						if((tD*tD)>.000001){
							running=true;
						}
						currRate[i]=nextRate[i];
						nextRate[i]=0;
					}
				}
				runs++;
			}
			double bestVal=-1;
			int bestVar=-1;
			for(int i=0;i<n;i++){
				if(!used[i]){
					if(degree[i]<2){
						currRate[i]=0;
					}
					if(currRate[i]>bestVal){
						bestVal=currRate[i];
						bestVar=i;
					}
				}
			}
			//cout << "Selected " << bestVar << " for phase " << VPC << endl;
			nextVar[VPC]=bestVar;
			used[bestVar]=true;
			for(list<int>::iterator iter=cross_link_list[bestVar].begin(); iter!=cross_link_list[bestVar].end(); iter++){
				degree[*iter]--;
				totalEdges-=2;
			}
		}
		hasRanked=true;
	}
	return nextVar[phase];
}


//PagerankD: Domain-based Pagerank algorithm.  It's slow, due to the
//massive floating-point operations.  It is roughly equivalent to
//H_X_Dom_Plus, where X is a limit of n^2.  In reality, it will end far
//before that due to convergence.
int BT::pagerankD(){
	
	//cout << "Starting PagerankD" << endl;
	static vector<double> currRate(n);
	static vector<double> nextRate(n);
	static vector<double> zeroRate(n);
	int bestVar = -1;
	double bestRate=-1;
	
	double totalEdges=0;
	for(int i=0;i<n;i++){
		//nextRate[i]=0;
		currRate[i]=vars[i].degree/vars[i].domainSize;
		totalEdges+=currRate[i];
	}
	for(int i=0;i<n;i++){
		//zeroRate[i]=currRate[i]=currRate[i]/totalEdges;
		currRate[i]=currRate[i]/totalEdges;
		zeroRate[i]=0;
		for(int m=0;m<vars[i].degree;m++)
			zeroRate[i]+=currRate[i];
		nextRate[i]=zeroRate[i];
	}
	//cout << "Starting Loop" << endl;
	double total;
	bool running=true;
	int runs=0;
	double tD;
	list<int>::iterator iter;
	while(running && runs<(n*n)){
		//cout << "Loop " << runs << endl;
		running=false;
		runs++;
		total=0;
		for(int i=0; i<n; i++){
			if(!this->isAssigned(i)){
				for(iter=cross_link_list[i].begin(); iter!=cross_link_list[i].end(); iter++){
					if(!this->isAssigned(*iter)){
						//nextRate[i]+=currRate[*iter]+zeroRate[i];
						nextRate[i]+=currRate[*iter];
					}
					//nextRate[i]+=vars[i].degree*zeroRate[i];
					//if(vars[i].degree>0)
					//	nextRate[i]/=vars[i].degree;
					total+=nextRate[i];
				}
			}
		}
		//cerr << "Finished Calc" << endl;
		for(int i=0;i<n;i++){
			if(!isAssigned(i)){
				nextRate[i]/=total;
				tD=currRate[i]-nextRate[i];
				if((tD*tD)>.000001)
					running=true;
				currRate[i]=nextRate[i];
				//nextRate[i]=0;
				nextRate[i]=zeroRate[i];
			}
		}
		//cerr << "Done Loop, " << (running?"Going Again":"Finished") << endl;
	}
	//cout << "Done Loop" << endl;
	for(int i=0;i<n;i++){
		//cout << i << endl;
		if(!this->isAssigned(i)){
			if(currRate[i]>bestRate || bestVar==-1){
				bestRate=currRate[i];
				bestVar=i;
			}
		}
	}
	return bestVar;
}				

//This is a Variable/Value function.  This function allows the 
//variable heuristic to select a different variable even within
//the same phase.  Degree and Pagerank do not benefit from this,
//as they are purely static
void BT::varNext(int& Var,int& Value)
{
	//cout << "Getting Variable." << endl;
	Var=CHOOSENEXTVAR();
	//cout << "Variable: " << Var << endl << "Getting Value." << endl;
	Value=NEXTVAL(Var,0);
	//cout << "Value: " << Value << endl;
}

//This is a Variable/Value function.  This function forces the 
//variable heuristic to stick with one variable per phase, though
//it does allow changes in the variable selection when moving
//forward.  This is the only function that allows Domain Splitting
void BT::varNextForceOld(int& Var,int& Value)
{
	if(phase>lastPhase)
	{
		//cout << "Phase: " << phase << endl;
		//cout << "Getting a new Variable: ";
		Var=CHOOSENEXTVAR();
		//cout << Var << endl;
#ifdef DOMAIN_SPLIT
		if(!initSplit())
			Value=-1;
#endif
	}
	//cout << "Getting a new Value: " ;
#ifdef DOMAIN_SPLIT
	if(Value!=-1)
#endif
		Value=NEXTVAL(Var,0);
	//cout << Value << endl;
	/*if(Value!=-1)
	{
		if(phase>lastPhase)
		{
			for(int i=0;i<phase;i++)
				cout << '>';
			cout << Var << "," << Value << endl;
		}
		else
		{
			for(int i=0;i<phase;i++)
				cout << ' ';
			cout << Value << endl;
		}
	}*/

	lastPhase=phase;
}

#ifdef VAL_COMPUTE
void BT::printCurrSupCon(int Var,int Val)
{
	cout << "Variable\tValue\t\tSupports\tConflicts" << endl;
	Domain *dp=vars[Var].dp;
	for(int v=dp[0].next;v!=0;v=dp[v].next)
	{
		if(v==Val)
		cout << "->" << Var;
		else
		cout << "  " << Var;

		cout << "\t\t" << v
			 << "\t\t" << currSup(Var,v)
			 << "\t\t" << currCon(Var,v) << endl;
	}
}

int BT::currSup(int Var,int Val)
{
	int support=0;
	for(list<int>::iterator iter=valConnect[Var*d+Val-1].begin();iter!=valConnect[Var*d+Val-1].end();iter++)
	{
		if(validValue(*iter))
			support++;
	}
		return support;
}

int BT::currCon(int Var,int Val)
{
	int conflict=0;
	for(list<int>::iterator iter=valConflict[Var*d+Val-1].begin();iter!=valConflict[Var*d+Val-1].end();iter++)
	{
		if(validValue(*iter))
			conflict++;
	}
	return conflict;
}
#endif

//This is a Variable/Value function.  It disregards the Value
//selector, and also performs backtrack variable forcing.
//This is the only function that allows non-pruning.
void BT::noPruneNext(int& Var,int& Value)
{
	if(phase>lastPhase)
	{
		Var=CHOOSENEXTVAR();
		Value=next(Var,0);
		//printCurrSupCon(Var,Value);
	}
	else
	{
		Value=next(Var,Value); //do not reselect variable for a given phase
		//printCurrSupCon(Var,Value);
	}
	lastPhase=phase;
}


#ifdef VAL_COMPUTE
//This is a Variable/Value function.  It performs both selections instead
//of relying on any other functions.  It requires pruning to work.  This
//version selects a variable by taking the variable with the largest conflict
//set value, and then chooses the value with the smallest conflict set of that
//variable.
void BT::valuerankVV(int& Var,int& Value)
{
	for(int i=0;i<n;i++)
	{
		currRankC[i]=0;
		if(!isAssigned(i))
		{
			Domain *dip=vars[i].dp;
			for(int vi=dip[0].next;vi!=0;vi=dip[vi].next)
			{
				for(list<int>::iterator iter=valConflict[i*d+vi-1].begin();iter!=valConflict[i*d+vi-1].end();iter++)
				{
					if(validValue(*iter))
					{
						currRankC[i]++;
					}
				}
			}
		}
	}
	double bestRank=-1; //less than all possible values
	for(int i=0;i<n;i++)
	{
		//cout << "Comparing Variable " << i << "(" << currRankC[i] << ") versus " << bestRank << endl;
		if(!isAssigned(i) && (currRankC[i]>bestRank))
		{
			Var=i;
			bestRank=currRankC[i];
		}
	}
	bestRank=n*d*d; //more than all possible values
	for(int vi=dp[0].next;vi!=0;vi=dp[vi].next)
	{
		if(currRankC[vi]<bestRank)
		{
			Value=vi;
			bestRank=currRankC[vi];
		}
	}
}




//This if a variable/Value function.  Selects the value with 
//the greatest product of supports to conflicts.  Easily changed
//to select the value with the greatest product of supports to conflicts
void BT::valuerank(int& Var,int& Value)
{
	for(int i=0;i<n*d;i++)
	{
		currRankS[i]=0;
		currRankC[i]=0;
	}
	for(int i=0;i<n;i++)
	{
		//cout << "Selecting " << i << " for initialization." << endl;
		if(!isAssigned(i)){
			Domain *dip=vars[i].dp;
			for(int vi=dip[0].next;vi!=0;vi=dip[vi].next)
			{
				for(list<int>::iterator iter=valConnect[i*d+vi-1].begin();iter!=valConnect[i*d+vi-1].end();iter++)
				{
					if(validValue(*iter))
						currRankS[i*d+vi-1]+=1;
				}
				for(list<int>::iterator iter=valConflict[i*d+vi-1].begin();iter!=valConflict[i*d+vi-1].end();iter++)
				{
					if(validValue(*iter))
						currRankC[i*d+vi-1]+=1;
				}

			}
		}
	}
	int bestVal=-1;
	double bestRank=-1;
	for(int i=0;i<n*d;i++)
	{
		if(validValue(i)&& (bestRank==-1 || bestRank<(currRankS[i]*(currRankC[i]+.000001))))
		{
			bestVal=i;
			bestRank=(currRankS[i]*(currRankC[i]+.000001));
		}
	}
	
	Var=bestVal/d;
	Value=bestVal%d+1;
}

//This is a value selector.  It chooses the value with the smallest
// conflict set/largest support set (roughly equivalent)
int BT::VVrankQ(int Var,int Value)
{
	
	Domain *dip=vars[Var].dp;
	int bestVal=1;
	int currVal;
	double bestRank=-1;
	for(int vi=dip[0].next;vi!=0;vi=dip[vi].next)
	{
		currVal=0;
		for(list<int>::iterator iter=valConflict[Var*d+vi-1].begin();iter!=valConflict[Var*d+vi-1].end();iter++)
		{
			if(validValue(*iter))
				currVal++;
		}
		if(bestRank>currVal || bestRank==-1)
		{
			bestVal=vi;
			bestRank=currVal;
		}
	}
	return bestVal;
}

//This is a value selector.  It chooses the value with the smallest
// conflict set/largest support set (roughly equivalent)
int BT::VVrank(int Var,int Value)
{
	
	//cout << "Initializing Rankings" << endl;
	//cout << "nextRank is " << &nextRank << endl;
	for(int i=0;i<n;i++)
	{
		//cout << "Selecting " << i << " for initialization." << endl;
		if(!isAssigned(i)){
			Domain *dip=vars[i].dp;
			for(int vi=dip[0].next;vi!=0;vi=dip[vi].next)
			{
				//cout << "Initializing (" << i << "," << vi << "), which is " << i*d+vi << " out of " << n*d << endl;
				currRankS[i*d+vi-1]=valConnect[i*d+vi-1].size();
				nextRankS[i*d+vi-1]=currRankS[i*d+vi-1];
				currRankC[i*d+vi-1]=valConflict[i*d+vi-1].size();
				nextRankC[i*d+vi-1]=currRankC[i*d+vi-1];
			}
		}
	}
	//cout << "Finished Initialization" << endl;
	bool running=true;
	int runs=0;
	double totalRankS,totalRankC;
	//while(running && runs<100)
	//{
		totalRankS=0;
		totalRankC=0;
		running=false;
		runs++;
		for(int i=0;i<n;i++)
		{
			//cout << "Ranking Variable" << i << endl;
			if(!isAssigned(i)){
				Domain *dip=vars[i].dp;
				for(int vi=dip[0].next;vi!=0;vi=dip[vi].next)
				{
					//cout << "Ranking Value " << vi << endl;
					for(list<int>::iterator iter=valConnect[i*d+vi-1].begin();iter!=valConnect[i*d+vi-1].end();iter++)
					{
						nextRankS[i*d+vi-1]+=currRankS[i*d+vi-1]+currRankS[*iter];
						nextRankC[i*d+vi-1]+=currRankC[i*d+vi-1]+currRankC[*iter];
						//cout << "Connected to (" << (*iter)/8 << "," << (*iter)%8 << ")" << endl;
					}
					//if(vars[i].degree>0)
						//nextRank[i*d+vi-1] /=vars[i].degree;
					totalRankS+=nextRankS[i*d+vi-1];
					totalRankC+=nextRankC[i*d+vi-1];
				}
			}
		}
		totalRankS/=1000; //the totalRank of a value graph is going to be massive.
		totalRankC/=1000; //this allows all values to be under 1000, keeping precision
		for(int i=0;i<n*d;i++)
		{
			if(totalRankS>0)
				nextRankS[i]=nextRankS[i]/totalRankS;
			if(totalRankC>0)
				nextRankS[i]=nextRankS[i]/totalRankS;
			double tD=nextRankS[i]-currRankS[i];
			if(tD*tD>.01)
				running=true;
			currRankS[i]=nextRankS[i];
			currRankC[i]=nextRankC[i];
			nextRankS[i]=nextRankC[i]=0;
		}
	//}

	int bestVal=-1;
	double bestRank=-1;
	for(int i=0;i<d;i++)
	{
		if(validValue(Var*d+i) && (bestRank==-1 || bestRank>currRankS[Var*d+i]))
		{
			bestVal=i;
			bestRank=currRankS[Var*d+i];
		}
	}
	return bestVal+1;
}

void BT::valuerank2(int& Var,int& Value)
{
	
	//cout << "Initializing Rankings" << endl;
	//cout << "nextRank is " << &nextRank << endl;
	for(int i=0;i<n;i++)
	{
		//cout << "Selecting " << i << " for initialization." << endl;
		if(!isAssigned(i)){
			Domain *dip=vars[i].dp;
			for(int vi=dip[0].next;vi!=0;vi=dip[vi].next)
			{
				//cout << "Initializing (" << i << "," << vi << "), which is " << i*d+vi << " out of " << n*d << endl;
				currRankS[i*d+vi-1]=currSup(i,vi);
				//cerr << "currRank Passed, value " << currRank[i*d+vi-1] << endl;
				nextRankS[i*d+vi-1]=0;
				
				currRankC[i*d+vi-1]=valConflict[i*d+vi-1].size();
			}
		}
	}
	//cout << "Finished Initialization" << endl;
	bool running=true;
	int runs=0;
	double totalRank;
	while(running && runs<100)
	{
		totalRank=0;
		running=false;
		runs++;
		for(int i=0;i<n;i++)
		{
			//cout << "Ranking Variable" << i << endl;
			if(!isAssigned(i)){
				Domain *dip=vars[i].dp;
				for(int vi=dip[0].next;vi!=0;vi=dip[vi].next)
				{
					//cout << "Ranking Value " << vi << endl;
					for(list<int>::iterator iter=valConnect[i*d+vi-1].begin();iter!=valConnect[i*d+vi-1].end();iter++)
					{
						nextRankS[i*d+vi-1]+=currRankS[i*d+vi-1]+currRankS[*iter];
						//cout << "Connected to (" << (*iter)/8 << "," << (*iter)%8 << ")" << endl;
					}
					//if(vars[i].degree>0)
						//nextRank[i*d+vi-1] /=vars[i].degree;
					totalRank+=nextRankS[i*d+vi-1];
				}
			}
		}
		totalRank/=1000; //the totalRank of a value graph is going to be massive.
						//this allows all values to be under 1000, keeping precision
		for(int i=0;i<n*d;i++)
		{
			if(totalRank>0)
				nextRankS[i]=nextRankS[i]/totalRank;
			double tD=nextRankS[i]-currRankS[i];
			if(tD*tD>.01)
				running=true;
			currRankS[i]=nextRankS[i];
			nextRankS[i]=0;
		}
	}

	int bestVal=-1;
	double bestRank=-1;
	for(int i=0;i<n*d;i++)
	{
		if(validValue(i)&& (/*bestRank==-1 || */bestRank<(currRankS[i]/(currRankC[i]+.000001))))
		{
			bestVal=i;
			bestRank=(currRankS[i]/(currRankC[i]+.000001));
		}
	}
	
	Var=bestVal/d;
	Value=bestVal%d+1;
}
#endif
//helper function for prune functions.  It determines if the ordered
//list y is a subset of the ordered list x.  Linear time on the 
//values in y
bool BT::currSubset(list<int>& x,list<int>& y)
{
	if(x.size()<y.size())
		return false;  //y must be smaller or equal to x to be a subset
	if(y.size()==0)
		return false;  //if y is empty, then subset doesn't matter.
	list<int>::iterator iterx,itery;
	iterx=x.begin();
	itery=y.begin();
	while(itery!=y.end()) //check smaller set
	{
		//for each element in y, there must be a corresponding element in x
		//this is relatively fast, as both lists are assumed sorted.
		if(validValue(*itery))
		{
			while((*itery)!=(*iterx) && iterx!=x.end())
			{
				iterx++; 
			}
		}
		if(iterx==x.end())
		{
			return false;
		}
		itery++;
	}
	return true;
}

#ifdef VAL_COMPUTE

//A prune function.  Does not work, due to massive logic errors.
//Kept for posterity.
void BT::pruneSimilar(int var,int val)
{
	pruneThese.clear();
	list<int> &supports=valConnect[var*d+val-1];
	list<int> &conflicts=valConflict[var*d+val-1];
	bool updating;
	for(int i=0;i<n;i++)
	{
		updating=false;
		if(!isAssigned(i))
		{
			for(int j=0;j<d;j++)
			{
				if(!validValue(i*d+j))
					continue;
				if((i==var && j == val-1) || (currSubset(supports,valConnect[i*d+j]) && currSubset(valConflict[var*d+j],conflicts)))
				{
					remove(i,j+1);
					
					if(!updating)
					{
						pruneThese.push_back(i);
						updating=true;
					}
					if(i!=var || j!= val-1)
					{
						//cout << "Pruned " << i << "," << j+1 << " due to failure of " << var << "," << val << endl;
						numPruned++;
					}
				}
			}
		}
	}
}

//A prune function.  Removes all values that are equivalent to the 
//failed value in support.  If a value's supports are a subset of
//the failed value's supports, then it cannot be part of the partial
//solution.
void BT::pruneVariable(int var,int val)
{
	pruneThese.clear();
	pruneThese.push_back(var);
	list<int> &supports=valConnect[var*d+val-1];
	for(int j=0;j<d;j++)
	{
		if(!validValue(var*d+j))
			continue;
		if((j == val-1) || currSubset(supports,valConnect[var*d+j)))
		{
			remove(var,j+1);
			if(j!= val-1)
			{
				//cout << "Pruned " << var << "," << j+1 << " due to failure of " << var << "," << val << endl;
				numPruned++;
			}
		}
	}
}
#endif

//A prune function.  Removes the failed value, and only the failed value.
void BT::pruneSingle(int var, int val)
{
	pruneThese.clear();
	//cout << "Single Removal." << endl;
	remove(var,val);
	if(vars[var].domainSize==0)
		autofail=true;
	pruneThese.push_back(var);
}

//A prune function.  Doesn't actually remove any value, but is required
//to produce proper functionality when using lazy heuristics.
void BT::pruneNone(int var,int val)
{
	pruneThese.clear();
	Domain *dp=vars[var].dp;
#if defined(TAIL_DOMAIN)// && !defined(ORDERED_DOMAIN)
	int i;
	for(i=val+1;i<=d;i++)
	{
		if(dp[i].yes)
			break;
	}
	if(i>d)
#else
	if(dp[val].next==0)
#endif
	{
		//cout << "Last Value for This Variable." << endl;
		autofail=true;
		pruneThese.push_back(var);
		//printDomain(var);
	}
}




